<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>HoareAsLogic: 证明论霍尔逻辑</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/plf.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://coq-zh.github.io/SF-zh/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 2: 编程语言基础</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>目录</li></a>
   <a href='coqindex.html'><li class='section_name'>索引</li></a>
   <a href='deps.html'><li class='section_name'>路线</li></a>
</ul>
</a></div>

<div id="main">

<h1 class="libtitle">HoareAsLogic<span class="subtitle">证明论霍尔逻辑</span></h1>


<div class="doc">

<div class="paragraph"> </div>

 在<a href="Hoare.html"><span class="inlineref">Hoare</span></a>一章中所介绍的霍尔逻辑可以被认为是“模型论”的：每一个构造子
    的证明规则以关于求值行为的<b>定理</b>的形式呈现，并且程序正确性（霍尔三元组的有
    效性）的证明由在Coq里面直接组合这些定理所构造。

<div class="paragraph"> </div>

    另外一种介绍霍尔逻辑的方式是定义一个完全分开的证明系统——关于命令，霍尔三元组
    等等的一系列公理和推断规则——接着说明霍尔三元组的一个证明是在<b>那个</b>逻辑中的一
    个合法导出式。这可以通过给出在这个新逻辑中的<b>合法导出式</b>的归纳定义来实现。

<div class="paragraph"> </div>

    这一章是可选的。在阅读之前，你会想要阅读一下在<b>逻辑基础</b>（<b>软件基础</b>的
    第一卷）中的 <a href="https://coq-zh.github.io/SF-zh/lf-current/ProofObjects.html"><span class="inlineref">ProofObjects</span></a> 章节。 
</div>
<div class="code code-tight">

<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Imp</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Hoare</span>.<br/>
</div>

<div class="doc">
<a name="lab128"></a><h1 class="section">定义</h1>

</div>
<div class="code code-space">

<br/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">hoare_proof</span> : <span class="id" type="var">Assertion</span> → <span class="id" type="var">com</span> → <span class="id" type="var">Assertion</span> → <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">H_Skip</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">P</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">hoare_proof</span> <span class="id" type="var">P</span> (<span class="id" type="var">SKIP</span>) <span class="id" type="var">P</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">H_Asgn</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Q</span> <span class="id" type="var">V</span> <span class="id" type="var">a</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">hoare_proof</span> (<span class="id" type="var">assn_sub</span> <span class="id" type="var">V</span> <span class="id" type="var">a</span> <span class="id" type="var">Q</span>) (<span class="id" type="var">V</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">a</span>) <span class="id" type="var">Q</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">H_Seq</span>  : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">P</span> <span class="id" type="var">c</span> <span class="id" type="var">Q</span> <span class="id" type="var">d</span> <span class="id" type="var">R</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">hoare_proof</span> <span class="id" type="var">P</span> <span class="id" type="var">c</span> <span class="id" type="var">Q</span> → <span class="id" type="var">hoare_proof</span> <span class="id" type="var">Q</span> <span class="id" type="var">d</span> <span class="id" type="var">R</span> → <span class="id" type="var">hoare_proof</span> <span class="id" type="var">P</span> (<span class="id" type="var">c</span>;;<span class="id" type="var">d</span>) <span class="id" type="var">R</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">H_If</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">P</span> <span class="id" type="var">Q</span> <span class="id" type="var">b</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">hoare_proof</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">st</span> ⇒ <span class="id" type="var">P</span> <span class="id" type="var">st</span> ∧ <span class="id" type="var">bassn</span> <span class="id" type="var">b</span> <span class="id" type="var">st</span>) <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">Q</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">hoare_proof</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">st</span> ⇒ <span class="id" type="var">P</span> <span class="id" type="var">st</span> ∧ ~(<span class="id" type="var">bassn</span> <span class="id" type="var">b</span> <span class="id" type="var">st</span>)) <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">Q</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">hoare_proof</span> <span class="id" type="var">P</span> (<span class="id" type="var">TEST</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">FI</span>) <span class="id" type="var">Q</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">H_While</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">P</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">hoare_proof</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">st</span> ⇒ <span class="id" type="var">P</span> <span class="id" type="var">st</span> ∧ <span class="id" type="var">bassn</span> <span class="id" type="var">b</span> <span class="id" type="var">st</span>) <span class="id" type="var">c</span> <span class="id" type="var">P</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">hoare_proof</span> <span class="id" type="var">P</span> (<span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span>) (<span class="id" type="keyword">fun</span> <span class="id" type="var">st</span> ⇒ <span class="id" type="var">P</span> <span class="id" type="var">st</span> ∧ ¬(<span class="id" type="var">bassn</span> <span class="id" type="var">b</span> <span class="id" type="var">st</span>))<br/>
&nbsp;&nbsp;| <span class="id" type="var">H_Consequence</span>  : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> <span class="id" type="var">Q</span> <span class="id" type="var">P'</span> <span class="id" type="var">Q'</span> : <span class="id" type="var">Assertion</span>) <span class="id" type="var">c</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">hoare_proof</span> <span class="id" type="var">P'</span> <span class="id" type="var">c</span> <span class="id" type="var">Q'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span>, <span class="id" type="var">P</span> <span class="id" type="var">st</span> → <span class="id" type="var">P'</span> <span class="id" type="var">st</span>) →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span>, <span class="id" type="var">Q'</span> <span class="id" type="var">st</span> → <span class="id" type="var">Q</span> <span class="id" type="var">st</span>) →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">hoare_proof</span> <span class="id" type="var">P</span> <span class="id" type="var">c</span> <span class="id" type="var">Q</span>.<br/>
</div>

<div class="doc">
我们并不需要包含对应 <span class="inlinecode"><span class="id" type="var">hoare_consequence_pre</span></span> 或 <span class="inlinecode"><span class="id" type="var">hoare_consequence_post</span></span> 的公理，
    因为它们可以简单地通过 <span class="inlinecode"><span class="id" type="var">H_Consequence</span></span> 被证明。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">H_Consequence_pre</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> <span class="id" type="var">Q</span> <span class="id" type="var">P'</span>: <span class="id" type="var">Assertion</span>) <span class="id" type="var">c</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">hoare_proof</span> <span class="id" type="var">P'</span> <span class="id" type="var">c</span> <span class="id" type="var">Q</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span>, <span class="id" type="var">P</span> <span class="id" type="var">st</span> → <span class="id" type="var">P'</span> <span class="id" type="var">st</span>) →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">hoare_proof</span> <span class="id" type="var">P</span> <span class="id" type="var">c</span> <span class="id" type="var">Q</span>.<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="id" type="tactic">eapply</span> <span class="id" type="var">H_Consequence</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">X</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>0</sub></span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">H_Consequence_post</span>  : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> <span class="id" type="var">Q</span> <span class="id" type="var">Q'</span> : <span class="id" type="var">Assertion</span>) <span class="id" type="var">c</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">hoare_proof</span> <span class="id" type="var">P</span> <span class="id" type="var">c</span> <span class="id" type="var">Q'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span>, <span class="id" type="var">Q'</span> <span class="id" type="var">st</span> → <span class="id" type="var">Q</span> <span class="id" type="var">st</span>) →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">hoare_proof</span> <span class="id" type="var">P</span> <span class="id" type="var">c</span> <span class="id" type="var">Q</span>.<br/>
<div class="togglescript" id="proofcontrol2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')"><span class="show"></span></div>
<div class="proofscript" id="proof2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="id" type="tactic">eapply</span> <span class="id" type="var">H_Consequence</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">X</span>. <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>0</sub></span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
作为一个例子，让我们构造一个证明对象，来表示这个霍尔三元组的一个导出式

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='letter-spacing:-.4em;'>{</span>{(<span class="id" type="var">X</span>=3)&nbsp;[<span class="id" type="var">X</span>&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span>&nbsp;<span class="id" type="var">X</span>&nbsp;+&nbsp;2]&nbsp;[<span class="id" type="var">X</span>&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span>&nbsp;<span class="id" type="var">X</span>&nbsp;+&nbsp;1]<span style='letter-spacing:-.4em;'>}</span>}<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span><span class="id" type="var">X</span>+1&nbsp;;;&nbsp;<span class="id" type="var">X</span><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span><span class="id" type="var">X</span>+2<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='letter-spacing:-.4em;'>{</span>{<span class="id" type="var">X</span>=3<span style='letter-spacing:-.4em;'>}</span>}.
<div class="paragraph"> </div>

</div>
    我们可以让 Coq 的策略来帮助我们构造这个证明对象。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">sample_proof</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">hoare_proof</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;((<span class="id" type="keyword">fun</span> <span class="id" type="var">st</span>:<span class="id" type="var">state</span> ⇒ <span class="id" type="var">st</span> <span class="id" type="var">X</span> = 3) [<span class="id" type="var">X</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span> <span class="id" type="var">X</span> + 2] [<span class="id" type="var">X</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span> <span class="id" type="var">X</span> + 1])<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 1;; <span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 2)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="keyword">fun</span> <span class="id" type="var">st</span>:<span class="id" type="var">state</span> ⇒ <span class="id" type="var">st</span> <span class="id" type="var">X</span> = 3).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">H_Seq</span>; <span class="id" type="tactic">apply</span> <span class="id" type="var">H_Asgn</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*<br/>
Print&nbsp;sample_proof.<br/>
<br/>
====&gt;<br/>
&nbsp;&nbsp;H_Seq<br/>
&nbsp;&nbsp;(((fun&nbsp;st&nbsp;:&nbsp;state&nbsp;=&gt;&nbsp;st&nbsp;X&nbsp;=&nbsp;3)&nbsp;<span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">+</span> <span class="inlinecode">2</span>)&nbsp;<span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">+</span> <span class="inlinecode">1</span>)<br/>
&nbsp;&nbsp;(X&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;X&nbsp;+&nbsp;1)<br/>
&nbsp;&nbsp;((fun&nbsp;st&nbsp;:&nbsp;state&nbsp;=&gt;&nbsp;st&nbsp;X&nbsp;=&nbsp;3)&nbsp;<span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">+</span> <span class="inlinecode">2</span>)<br/>
&nbsp;&nbsp;(X&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;X&nbsp;+&nbsp;2)<br/>
&nbsp;&nbsp;(fun&nbsp;st&nbsp;:&nbsp;state&nbsp;=&gt;&nbsp;st&nbsp;X&nbsp;=&nbsp;3)<br/>
&nbsp;&nbsp;(H_Asgn<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;((fun&nbsp;st&nbsp;:&nbsp;state&nbsp;=&gt;&nbsp;st&nbsp;X&nbsp;=&nbsp;3)&nbsp;<span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">+</span> <span class="inlinecode">2</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;X&nbsp;(X&nbsp;+&nbsp;1))<br/>
&nbsp;&nbsp;(H_Asgn<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(fun&nbsp;st&nbsp;:&nbsp;state&nbsp;=&gt;&nbsp;st&nbsp;X&nbsp;=&nbsp;3)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;X&nbsp;(X&nbsp;+&nbsp;2))<br/>
*)</span><br/>
</div>

<div class="doc">
<a name="lab129"></a><h1 class="section">性质</h1>

<div class="paragraph"> </div>

<a name="lab130"></a><h4 class="section">练习：2 星, standard (hoare_proof_sound)</h4>
 证明这些证明对象是正确的断言。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">hoare_proof_sound</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">P</span> <span class="id" type="var">c</span> <span class="id" type="var">Q</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">hoare_proof</span> <span class="id" type="var">P</span> <span class="id" type="var">c</span> <span class="id" type="var">Q</span> → <span style='letter-spacing:-.4em;'>{</span>{<span class="id" type="var">P</span><span style='letter-spacing:-.4em;'>}</span>} <span class="id" type="var">c</span> <span style='letter-spacing:-.4em;'>{</span>{<span class="id" type="var">Q</span><span style='letter-spacing:-.4em;'>}</span>}.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 我们也可以使用Coq的推理工具来证明关于霍尔逻辑的元定理。例如，下述是我们在
    <a href="Hoare.html"><span class="inlineref">Hoare</span></a> 章节中看到的两条定理的模拟——这一次，使用霍尔逻辑导出式（可证明
    性），而不是直接使用霍尔三元组的语义，来表达这些定理。

<div class="paragraph"> </div>

    第一条定理表达，对于所有的 <span class="inlinecode"><span class="id" type="var">P</span></span> 和 <span class="inlinecode"><span class="id" type="var">c</span></span>，断言 <span class="inlinecode"><span style='letter-spacing:-.4em;'>{</span>{<span class="id" type="var">P</span><span style='letter-spacing:-.4em;'>}</span>}</span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span style='letter-spacing:-.4em;'>{</span>{<span class="id" type="var">True</span><span style='letter-spacing:-.4em;'>}</span>}</span> 在霍尔逻辑中是
    <b>可证明的</b>。注意到这个证明比在<span class="inlinecode"><span class="id" type="var">Hoare</span></span>中的语义证明更加复杂：实际上我们需要在命令
    <span class="inlinecode"><span class="id" type="var">c</span></span> 的结构上应用归纳法 。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">H_Post_True_deriv</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">c</span> <span class="id" type="var">P</span>, <span class="id" type="var">hoare_proof</span> <span class="id" type="var">P</span> <span class="id" type="var">c</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">_</span> ⇒ <span class="id" type="var">True</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intro</span> <span class="id" type="var">c</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">c</span>; <span class="id" type="tactic">intro</span> <span class="id" type="var">P</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;SKIP&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">H_Consequence</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">H_Skip</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;Proof&nbsp;of&nbsp;True&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">I</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">H_Consequence_pre</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">H_Asgn</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">I</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;;;&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">H_Consequence_pre</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">H_Seq</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> (<span class="id" type="var">IHc1</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">_</span> ⇒ <span class="id" type="var">True</span>)).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHc2</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">I</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;TEST&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">H_Consequence_pre</span> <span class="id" type="keyword">with</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">_</span> ⇒ <span class="id" type="var">True</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">H_If</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHc1</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHc2</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">I</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;WHILE&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">H_Consequence</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">H_While</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">IHc</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span>; <span class="id" type="tactic">apply</span> <span class="id" type="var">I</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span>; <span class="id" type="tactic">apply</span> <span class="id" type="var">I</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
类似地，我们可以说明对于任意的 <span class="inlinecode"><span class="id" type="var">c</span></span> 和 <span class="inlinecode"><span class="id" type="var">Q</span></span>，<span class="inlinecode"><span style='letter-spacing:-.4em;'>{</span>{<span class="id" type="var">False</span><span style='letter-spacing:-.4em;'>}</span>}</span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span style='letter-spacing:-.4em;'>{</span>{<span class="id" type="var">Q</span><span style='letter-spacing:-.4em;'>}</span>}</span> 是可证明的。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">False_and_P_imp</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">P</span> <span class="id" type="var">Q</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">False</span> ∧ <span class="id" type="var">P</span> → <span class="id" type="var">Q</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">P</span> <span class="id" type="var">Q</span> [<span class="id" type="var">CONTRA</span> <span class="id" type="var">HP</span>].<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">CONTRA</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Tactic Notation</span> "pre_false_helper" <span class="id" type="var">constr</span>(<span class="id" type="var">CONSTR</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">H_Consequence_pre</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" type="tactic">eapply</span> <span class="id" type="var">CONSTR</span> | <span class="id" type="tactic">intros</span> ? <span class="id" type="var">CONTRA</span>; <span class="id" type="tactic">destruct</span> <span class="id" type="var">CONTRA</span>].<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">H_Pre_False_deriv</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">c</span> <span class="id" type="var">Q</span>, <span class="id" type="var">hoare_proof</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">_</span> ⇒ <span class="id" type="var">False</span>) <span class="id" type="var">c</span> <span class="id" type="var">Q</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">c</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">c</span>; <span class="id" type="tactic">intro</span> <span class="id" type="var">Q</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;SKIP&nbsp;*)</span> <span class="id" type="var">pre_false_helper</span> <span class="id" type="var">H_Skip</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;*)</span> <span class="id" type="var">pre_false_helper</span> <span class="id" type="var">H_Asgn</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;;;&nbsp;*)</span> <span class="id" type="var">pre_false_helper</span> <span class="id" type="var">H_Seq</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">IHc1</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">IHc2</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;TEST&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">H_If</span>; <span class="id" type="tactic">eapply</span> <span class="id" type="var">H_Consequence_pre</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHc1</span>. <span class="id" type="tactic">intro</span>. <span class="id" type="tactic">eapply</span> <span class="id" type="var">False_and_P_imp</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHc2</span>. <span class="id" type="tactic">intro</span>. <span class="id" type="tactic">eapply</span> <span class="id" type="var">False_and_P_imp</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;WHILE&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">H_Consequence_post</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">H_While</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">H_Consequence_pre</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHc</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intro</span>. <span class="id" type="tactic">eapply</span> <span class="id" type="var">False_and_P_imp</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intro</span>. <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">eapply</span> <span class="id" type="var">False_and_P_imp</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
最后，我们可以说明 <span class="inlinecode"><span class="id" type="var">hoare_proof</span></span> 公理集合足够用来证明关于任何（部分）正确性的
    事实。更准确地说，任何我们能够证明的语义霍尔三元组，都能够通过这些公理证明。
    这样的公理集合被称为<b>相对完备的（relatively complete）</b>。我们的证明的灵感来自
    于：

<div class="paragraph"> </div>

      <a href="https://www.ps.uni-saarland.de/courses/sem-ws<sub>11</sub>/script/Hoare.html"><span class="inlineref">https://www.ps.uni-saarland.de/courses/sem-ws<sub>11</sub>/script/Hoare.html</span></a>

<div class="paragraph"> </div>

    为了完成这个证明，我们需要使用一种被称为
    <b>最弱前置条件（weakest preconditions）</b>的技术装置来创造一些中间的断言。

<div class="paragraph"> </div>

    给定一个命令<span class="inlinecode"><span class="id" type="var">c</span></span>和一个想要的后置条件断言 <span class="inlinecode"><span class="id" type="var">Q</span></span> ，最弱前置条件 <span class="inlinecode"><span class="id" type="var">wp</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">Q</span></span> 是一个断言
    <span class="inlinecode"><span class="id" type="var">P</span></span>，使得 <span class="inlinecode"><span style='letter-spacing:-.4em;'>{</span>{<span class="id" type="var">P</span><span style='letter-spacing:-.4em;'>}</span>}</span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span style='letter-spacing:-.4em;'>{</span>{<span class="id" type="var">Q</span><span style='letter-spacing:-.4em;'>}</span>}</span> 成立，并且对于任意其他断言 <span class="inlinecode"><span class="id" type="var">P'</span></span>，如果 <span class="inlinecode"><span style='letter-spacing:-.4em;'>{</span>{<span class="id" type="var">P</span><span style='letter-spacing:-.4em;'>}</span>}</span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span style='letter-spacing:-.4em;'>{</span>{<span class="id" type="var">Q</span><span style='letter-spacing:-.4em;'>}</span>}</span> 成立，那么
    <span class="inlinecode"><span class="id" type="var">P'</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">P</span></span>。我们可以更加直接地将其定义为： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">wp</span> (<span class="id" type="var">c</span>:<span class="id" type="var">com</span>) (<span class="id" type="var">Q</span>:<span class="id" type="var">Assertion</span>) : <span class="id" type="var">Assertion</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">fun</span> <span class="id" type="var">s</span> ⇒ <span style='font-size:120%;'>&forall;</span><span class="id" type="var">s'</span>, <span class="id" type="var">s</span> =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">s'</span> → <span class="id" type="var">Q</span> <span class="id" type="var">s'</span>.<br/>
</div>

<div class="doc">
<a name="lab131"></a><h4 class="section">练习：1 星, standard (wp_is_precondition)</h4>

</div>
<div class="code code-space">

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">wp_is_precondition</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c</span> <span class="id" type="var">Q</span>,<br/>
&nbsp;&nbsp;<span style='letter-spacing:-.4em;'>{</span>{<span class="id" type="var">wp</span> <span class="id" type="var">c</span> <span class="id" type="var">Q</span><span style='letter-spacing:-.4em;'>}</span>} <span class="id" type="var">c</span> <span style='letter-spacing:-.4em;'>{</span>{<span class="id" type="var">Q</span><span style='letter-spacing:-.4em;'>}</span>}.<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab132"></a><h4 class="section">练习：1 星, standard (wp_is_weakest)</h4>

</div>
<div class="code code-space">

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">wp_is_weakest</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c</span> <span class="id" type="var">Q</span> <span class="id" type="var">P'</span>,<br/>
&nbsp;&nbsp;&nbsp;<span style='letter-spacing:-.4em;'>{</span>{<span class="id" type="var">P'</span><span style='letter-spacing:-.4em;'>}</span>} <span class="id" type="var">c</span> <span style='letter-spacing:-.4em;'>{</span>{<span class="id" type="var">Q</span><span style='letter-spacing:-.4em;'>}</span>} → <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span>, <span class="id" type="var">P'</span> <span class="id" type="var">st</span> → <span class="id" type="var">wp</span> <span class="id" type="var">c</span> <span class="id" type="var">Q</span> <span class="id" type="var">st</span>.<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
下面这个辅助引理也很有用。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">bassn_eval_false</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">st</span>, ¬<span class="id" type="var">bassn</span> <span class="id" type="var">b</span> <span class="id" type="var">st</span> → <span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b</span> = <span class="id" type="var">false</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">b</span> <span class="id" type="var">st</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">bassn</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">destruct</span> (<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">exfalso</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab133"></a><h4 class="section">练习：5 星, standard (hoare_proof_complete)</h4>
 完成如下定理的证明。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">hoare_proof_complete</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">P</span> <span class="id" type="var">c</span> <span class="id" type="var">Q</span>,<br/>
&nbsp;&nbsp;<span style='letter-spacing:-.4em;'>{</span>{<span class="id" type="var">P</span><span style='letter-spacing:-.4em;'>}</span>} <span class="id" type="var">c</span> <span style='letter-spacing:-.4em;'>{</span>{<span class="id" type="var">Q</span><span style='letter-spacing:-.4em;'>}</span>} → <span class="id" type="var">hoare_proof</span> <span class="id" type="var">P</span> <span class="id" type="var">c</span> <span class="id" type="var">Q</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">P</span> <span class="id" type="var">c</span>. <span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">P</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">c</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">P</span> <span class="id" type="var">Q</span> <span class="id" type="var">HT</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;SKIP&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">H_Consequence</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">H_Skip</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="id" type="var">eassumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intro</span> <span class="id" type="var">st</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">HT</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">E_Skip</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">H_Consequence</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">H_Asgn</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intro</span> <span class="id" type="var">st</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">HT</span>. <span class="id" type="var">econstructor</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span>; <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;;;&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">H_Seq</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">wp</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">Q</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">IHc1</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">E<sub>1</sub></span> <span class="id" type="var">H</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">wp</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">st''</span> <span class="id" type="var">E<sub>2</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">HT</span>. <span class="id" type="var">econstructor</span>; <span class="id" type="var">eassumption</span>. <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">IHc2</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">E<sub>1</sub></span> <span class="id" type="var">H</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 最后，我们可能希望我们的公理霍尔逻辑是<b>可决定的（decidable）</b>；也就是说，这里
    有一个（会终止的）算法（一个<b>决定性过程（decision procedure）</b>）来决定一个给
    定的霍尔三元组是否是合法的（可导出的）。但是这样的一个决定性过程并不存在！

<div class="paragraph"> </div>

    考虑三元组 <span class="inlinecode"><span style='letter-spacing:-.4em;'>{</span>{<span class="id" type="var">True</span><span style='letter-spacing:-.4em;'>}</span>}</span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span style='letter-spacing:-.4em;'>{</span>{<span class="id" type="var">False</span><span style='letter-spacing:-.4em;'>}</span>}</span>。这个三元组是有效的当且仅当 <span class="inlinecode"><span class="id" type="var">c</span></span> 不终止。这意味着，
    任何一个能够决定任意三元组的合法性的算法能够解决停机问题（Halting Problem）。

<div class="paragraph"> </div>

    类似地，三元组 <span class="inlinecode"><span style='letter-spacing:-.4em;'>{</span>{<span class="id" type="var">True</span><span style='letter-spacing:-.4em;'>}</span>}</span> <span class="inlinecode"><span class="id" type="var">SKIP</span></span> <span class="inlinecode"><span style='letter-spacing:-.4em;'>{</span>{<span class="id" type="var">P</span><span style='letter-spacing:-.4em;'>}</span>}</span> 是合法的当且仅当 <span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span> <span class="inlinecode"><span class="id" type="var">s</span>,</span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">s</span></span> 是合法的，其中 <span class="inlinecode"><span class="id" type="var">P</span></span>
    是Coq逻辑的任意一个断言。但是我们已知对于这个逻辑并没有任何的决定性过程。

<div class="paragraph"> </div>

    总而言之，此公理化表述更清晰地诠释如何“出具霍尔逻辑下的证明”。
    但是，从实际上我们需要写出这些证明的角度来看，这并不让人完全
    满意：这太冗长了。在 <a href="Hoare2.html"><span class="inlineref">Hoare2</span></a> 一章中的关于形式化修饰程序的章节会向我们展
    示如何做的更好。 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Oct&nbsp;28&nbsp;08:15:18&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>



</div>

</body>
</html>